| Definitions | t  T,  b, E, x:A  B(x), P   Q, type List, s = t, {x:A| B(x)} , E(X), let x,y = A in B(x;y), t.1,  x:A. B(x), a:A fp B(a), strong-subtype(A;B), ES, Type, AbsInterface(A), sys-antecedent(es;Sys), [car / cdr],  , no_repeats(T;l), x:A  B(x), P & Q, left + right, P  Q, <a, b>, adjacent(T;L;x;y),  x:A. B(x), False, a < b,  A, increasing(f;k), L1  L2, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , Atom$n, Top, last(L), hd(l), X(e), e  X,  ,  , Outcome, #$n, A  B, ||as||, !Void(),  , l[i], |g|, S T, A c B, [], P  Q, True, i  j , n+m, i j < k, {i..j }, (e <loc e'),  x:A.B(x), suptype(S; T), e < e', (e < e'), Unit, ff, inr x , tt, inl x , e c e', -n, n - m, null(as), b, p =b q, i <z j, i z j, (i = j), x =a y, a < b, x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), e = e', p q, p q, p q, chain-consistent(f;chain), EState(T),  , EqDecider(T), IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r s, constant_function(f;A;B), SWellFounded(R(x;y)), pred!(e;e'),   x,y. t(x;y), first(e), pred(e), x.A(x), x. t(x), Id, f(a), loc(e), (x l) |
| Lemmas | non neg length, es-causle wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, val-axiom wf, cless wf, qle wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, first wf, pred! wf, strongwellfounded wf, rationals wf, EState wf, event system wf, no repeats wf, ifthenelse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, es-interface-val wf2, es-interface-val wf, hd wf, adjacent wf, sys-antecedent wf, es-interface wf, btrue wf, bfalse wf, unit wf, bool wf, es-is-interface wf, es-E-interface-subtype rel, last wf, assert wf, sublist wf, es-causl wf, es-locl wf, increasing wf, length wf nat, top wf, int seg wf, le wf, ge wf, true wf, nil member, length wf2, not wf, false wf, nat wf, length wf1, select wf, Id wf, l member wf, es-loc wf, member wf, es-E wf, es-E-interface wf, subtype rel wf |